 Process
Analysis Toolkit (PAT) 3.5
Help |
Exp ::=
(Expression)
(Ext)* (Gvar)* {E} E
(Define)* (Assert)*
Ext ::=
(External Site)
ExternalSite
X(P,..,P)([haltAllow{TimeREx}])?{TimeEx}
(external site header)
(SVar)*
(system variable declaration)
{E}
(system variable initialization)
E
(external site body)
EndSite
(external site footer)
TimeREx ::=
(Time Range Expression)
(Integer,Integer)
(time range tuple)
| inf
(infinity/non-response)
TimeEx ::=
(Time Expression)
Integer,...,Integer
(time List)
GVar ::=
(Global Variable)
globalvar X(=P)?
(global variable declarartion)
SVar ::=
(System Variable)
systemvar X(=P)?
(system variable declarartion)
E ::=
(ORC Expression)
C
(constant value)
| X
(variable)
| stop
(silent expression)
| ( E , ... , E
)
(tuple)
| [ E , ... , E ]
(list)
| E G+
(call)
| op E
(prefix operator)
| E op E
(infix operator)
| if E then E
else E
(conditional)
| E >P> E
(sequential combinator)
| E | E
(parallel combinator)
| E <P< E
(pruning combinator)
| E ; E
(otherwise combinator)
G ::=
(Argument group)
( E , ...
, E )
(arguments)
| .
(field field access)
C ::=
(Constant)
Boolean
| Integer
| String
| signal
| null
X ::=
(Variable)
Identifier
D ::=
(Declaration)
val P = E
(value declaration)
| def X( P ,
... , P ) = E
(function declaration)
P ::=
(Pattern)
X
(variable)
| C
(constant)
| _
(wildcard)
| ( P , ... ,
P )
(tuple pattern)
| [ P , ... ,
P ]
(list pattern)
| P : P
(cons pattern)
Define:=
(Condition Definition)
#define X (E)
Assert:=
(Assertion)
#assert System
(deadlockfree
(deadlock-freeness check)
| reaches X
(reachability check)
| |= LTL
(ltl check)
| nrsdeadlockfree
(nrsdeadlock-freeness check)
| nrscyclefree)
(nrscycle-freeness check)
LTL:=
(LTL Expression)
"C"
(publish value)
| X
(predefined condition)
|[] LTL
(always)
|<> LTL
(eventually)
|X LTL
(next)
|LTL U LTL
(until)
|LTL R LTL
(release)
Copyright © 2007-2012 Semantic Engineering Pte. Ltd.